// Copyright 2007-2009, Stanford University. All Rights Reserved.
// Copyright 2010-2011, Dependable Systems Lab, EPFL. All Rights Reserved.
// Copyright 2012, Google Inc. All Rights Reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
//
//     * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimers.
//     * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimers
// in the documentation and/or other materials provided with the
// distribution.
//     * Neither the names of the klee Team, Stanford University, nor the
// names of its contributors may be used to endorse or promote
// products derived from the software without specific prior
// written permission. Neither the names of the Dependable Systems
// Laboratory, EPFL, nor the names of its contributors may be used to
// endorse or promote products derived from the software without prior
// written permission. Neither the names of Google Inc. nor the names of
// its contributors may be used to endorse or promote products derived from
// the software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

#ifndef SRC_SOLVER_SOLVERIMPL_H_
#define SRC_SOLVER_SOLVERIMPL_H_

#include <vector>

#include "util/Ref.h"

namespace seven_summits {
namespace expr {
class Array;
class ExecutionState;
class Expr;
struct Query;
}
}

namespace seven_summits {
namespace solver {

using expr::Array;
using util::ref;

/// SolverImpl - Abstract base clase for solver implementations.
class SolverImpl {
  // DO NOT IMPLEMENT.
  SolverImpl(const SolverImpl&);
  void operator=(const SolverImpl&);

public:
  SolverImpl() {}
  virtual ~SolverImpl() {}

  /// computeValidity - Compute a full validity result for the
  /// query.
  ///
  /// The query expression is guaranteed to be non-constant and have
  /// bool type.
  ///
  /// SolverImpl provides a default implementation which uses
  /// computeTruth. Clients should override this if a more efficient
  /// implementation is available.
  virtual bool computeValidity(const Query& query, Solver::Validity &result);

  /// computeTruth - Determine whether the given query is provable.
  ///
  /// The query expression is guaranteed to be non-constant and have
  /// bool type.
  virtual bool computeTruth(const Query& query, bool &isValid) = 0;

  /// computeValue - Compute a feasible value for the expression.
  ///
  /// The query expression is guaranteed to be non-constant.
  virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;

  virtual bool computeInitialValues(const Query& query,
                                    const std::vector<const Array*>
                                      &objects,
                                    std::vector< std::vector<unsigned char> >
                                      &values,
                                    bool &hasSolution) = 0;
};

} // namespace solver
} // namespace seven_summits

#endif  // SRC_SOLVER_SOLVERIMPL_H_
